; COMMAND-LINE: --incremental
; EXPECT: sat

(set-logic QF_UFLIA)
(set-info :smt-lib-version 2.6)
(declare-fun _base () Int)
(declare-fun _n () Int)
(declare-fun ___z3z___ (Int) Bool)
(declare-fun ___z4z___ (Int) Bool)
(declare-fun ___z6z___ (Int) Bool)
(declare-fun ___z8z___ (Int) Bool)
(declare-fun ___z9z___ (Int) Bool)
(declare-fun ___z11z___ (Int) Bool)
(declare-fun ___z12z___ (Int) Int)
(declare-fun ___z14z___ (Int) Int)
(declare-fun ___z15z___ (Int) Int)
(declare-fun ___z16z___ (Int) Bool)
(declare-fun ___z19z___ (Int) Bool)
(declare-fun ___z20z___ (Int) Bool)
(declare-fun ___z22z___ (Int) Bool)
(declare-fun ___z24z___ (Int) Bool)
(declare-fun ___z25z___ (Int) Bool)
(assert (= (and (<= 1 (+ (___z14z___ (- 1)) (___z15z___ (- 1)))) (<= 1 (___z12z___ (- 1)))) (___z20z___ 0)))
(assert (= (or (not (___z16z___ 0)) (<= 0 (___z15z___ 0))) (___z11z___ 0)))
(assert (let ((?v_2 (___z14z___ (- 1))) (?v_0 (___z15z___ (- 1)))) (let ((?v_1 (+ 2 ?v_0))) (= (___z15z___ 0) (ite (= _base 0) 0 (ite (___z3z___ 0) (ite (___z19z___ 0) ?v_1 ?v_0) (ite (___z4z___ 0) (ite (___z20z___ 0) (+ 1 (+ ?v_2 (+ (- 1) ?v_0))) ?v_0) (ite (___z6z___ 0) (ite (___z22z___ 0) 0 ?v_0) (ite (___z8z___ 0) (ite (___z24z___ 0) ?v_1 ?v_0) (ite (___z9z___ 0) (ite (___z25z___ 0) (+ 1 (+ ?v_2 ?v_0)) ?v_0) ?v_0))))))))))
(assert (= (and (<= 1 (+ (___z14z___ (- 1)) (___z15z___ (- 1)))) (<= 1 (___z12z___ (- 1)))) (___z25z___ 0)))
(assert (= (or (not (___z16z___ (- 1))) (<= 0 (___z15z___ (- 1)))) (___z11z___ (- 1))))
(assert (let ((?v_2 (___z14z___ (- 2))) (?v_0 (___z15z___ (- 2)))) (let ((?v_1 (+ 2 ?v_0))) (= (___z15z___ (- 1)) (ite (= _base (- 1)) 0 (ite (___z3z___ (- 1)) (ite (___z19z___ (- 1)) ?v_1 ?v_0) (ite (___z4z___ (- 1)) (ite (___z20z___ (- 1)) (+ 1 (+ ?v_2 (+ (- 1) ?v_0))) ?v_0) (ite (___z6z___ (- 1)) (ite (___z22z___ (- 1)) 0 ?v_0) (ite (___z8z___ (- 1)) (ite (___z24z___ (- 1)) ?v_1 ?v_0) (ite (___z9z___ (- 1)) (ite (___z25z___ (- 1)) (+ 1 (+ ?v_2 ?v_0)) ?v_0) ?v_0))))))))))
(push 1)
(assert (not (or (not (= _base (- 1))) (and (___z11z___ 0) (___z11z___ (- 1))))))
(pop 1)
(check-sat)
